$\forall$$i$:Id, $l$:IdLnk, ${\it tg}$, $n$, $f$, $k$:Top.
\\[0ex]msg{-}spec{-}loc($k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$;$i$) $\Leftrightarrow$ source($l$) $=$ $i$